In shared-memory concurrent programming, shared resources can be protectedusing synchronization mechanisms such as monitors or channels. The connectionbetween these mechanisms and the resources they protect is, however, only givenimplicitly; this makes it difficult both for programmers to apply themechanisms correctly and for compilers to check that resources are properlyprotected. This paper presents a mechanism to automatically check that sharedmemory is accessed properly, using a methodology called shared ownership. Incontrast to traditional ownership, shared ownership offers more flexibility bypermitting multiple owners of a resource. On the basis of this methodology, wedefine an abstract model of resource access that provides operations to managedata dependencies, as well as sharing and transfer of access privileges. Themodel is rigorously defined using a formal semantics, and shown to be free fromdata races. This property can be used to detect unsafe memory accesses whensimulating the model together with the execution of a program. Theexpressiveness and efficiency of the approach is demonstrated on a variety ofprograms using common synchronization mechanisms.
展开▼
